\begin{tabbing}
@$i$[[$x$;${\it snd}$]]
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=es{-}decls(${\it es}$;$i$;${\it ds}$;${\it da}$)\+
\\[0ex]$\Rightarrow$ \=with decls \=${\it ds}$ \+\+
\\[0ex]${\it da}$
\-\\[0ex]sends on $l$ from $e$ 
\\[0ex]include tagged{-}list{-}messages(\=(state when $e$);\+
\\[0ex]val($e$);
\\[0ex]mapfilter(\=$\lambda$${\it tr}$.$\langle$1of(${\it tr}$)$,\,$2of(2of(${\it tr}$))$\rangle$;\+
\\[0ex]$\lambda$${\it tr}$.action[[$x$ 1of(\=2of(\+
\\[0ex]${\it tr}$))]][es{-}init(${\it es}$;$e$);$e$];
\-\\[0ex]${\it snd}$($\langle$kind($e$)$,\,$$l$$\rangle$)?nil)) 
\-\-\\[0ex]and only these for tags in ecl{-}tags($l$;${\it snd}$)
\-\-
\end{tabbing}